-- Parameter used as return type
    DEF def1(X:nat, Y:nat):nat == IF true THEN X ELSE Y FI
    DEF def2(X:nat):nat == X
    DEF def4(X:nat, Y:nat, Z:nat):nat == add(X,Y)
    DEF MAIN:bool == true
    DEF X(X:bool):nat == 1
    DEF Y():nat == X(true)
